A:Type, I:MaInterface(A), i:{i:Id| (i  fpf-domain(I))} .
I(i)  (ds:x:Id fp Type  k:{k:Knd| hasloc(k;i)}  fp V:Type  (State(ds)V(A + Top))) 

latex

Definitions	Id, type List, (x  l), {x:A| B(x)} , Type, x:AB(x), x:A  B(x), a:A fp B(a), t  T, x:A. B(x), S  T, Top, left + right, State(ds), Knd, b, hasloc(k;i), x.A(x), x. t(x), t.1, t.2, f(a), f(x), fpf-domain(f), MaInterface(T)
Lemmas	pi2 wf, pi1 wf, Id wf, Knd wf, assert wf, hasloc wf, l member wf, decl-state wf, top wf